M1, M2:MsgA. M1  M2  (k:Knd, x:Id. M2.frame(k affects x)  M1.frame(k affects x)) 

latex

Definitions	M.frame(k affects x), M1  M2, MsgA, Valtype(da;k), P & Q, z != f(x)  P(a;z), x  dom(f), IdDeq, a:A fp B(a), x. t(x), b, , Prop, deq-member(eq;x;L), EqDecider(T), T, True, KindDeq, Knd, f(x), Id, IdLnk, t  T, f  g, x:A. B(x), P  Q, A & B
Lemmas	Kind-deq wf, Knd wf, deq wf, true wf, squash wf, deq-member wf, bool wf, assert wf, fpf-trivial-subtype-top, id-deq wf, Id wf, fpf-dom wf, msga wf, ma-sub wf, ma-frame wf